FDL - Step of Proof: nat_ind

Step of Proof: nat_ind_tp

9,38

Inference at * 1 1 1
Iof proof for Lemma nat ind tp:

1. P :

{k}
2. P(0)
3.

. P(i - 1)

P(i)
4. i :

5. i

P(i)

by (\p.IntInd (get_int_arg `hn` p) p)

1: .....downcase..... NILNIL

1: 5. i < 0

1: 6. ((i + 1)

0 )

P(i + 1)

0 )

P(i)

2: .....basecase..... NILNIL

2: 3.

. P(i - 1)

P(i)

0 )

P(0)

3: .....upcase..... NILNIL

3: 5. 0 < i

3: 6. ((i - 1)

0 )

P(i - 1)

0 )

P(i)

Definitions P Q